Nuprl Definition : d-single-pre
0,22
postcript
pdf
@
i
(with ds:
ds
action
a
:
T
precondition
a
(v) is
P
s v)(
j
)
== if eqof(IdDeq)(
j
,
i
)
(with ds:
ds
action
a
:
T
precondition
a
(v) is
P
s v) else fi
latex
Definitions
,
(with ds:
ds
action
a
:
T
precondition
a
(v) is
P
s v)
,
IdDeq
,
eqof(
d
)
,
if
b
t
else
f
fi
FDL editor aliases
d-single-pre
origin
(with ds: ds action a:T precondition a(v) is P s v) else fi (with ds: ds action a:T precondition a(v) is P s v) else fi t else f fi